es:event_system{i:l}, i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type).
es-decls(es;i;ds;da)
 guard(((x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
 guard( (e:es-E(es). 
 guard( ((loc(e) = i)  (es-isrcv(es; e)))
 guard(  subtype_rel(es-valtype(es; e); fpf-cap(da; Kind-deq; es-kind(es; e); top))))) 

latex

Definitions

P  Q, P  Q, es-decls(es;i;ds;da), guard(T), P  Q, es-vartype(es; i; x), id-deq, es-E(es), P  Q, P  Q, loc(e), b, es-isrcv(es; e), es-valtype(es; e), fpf-cap(f; eq; x; z), Kind-deq, es-kind(es; e), top, Knd, fpf(A; a.B(a)), x:A. B(x), x. t(x), Id, t  T, event_system{i:l}, fpf-domain(f), let x = a in b(x), fpf-ap(f; eq; x), prop{i:l}, EqDecider(T), (x  l), Unit, fpf-dom(eq; x; f), , b, A, l_all(L; T; x.P(x)), if b then t else f fi , l-all(L; x.P(x)), sq_type(T), False

Lemmas

Knd sq, bool sq, bool cases, not wf, bnot wf, bool wf, deq wf, subtype rel self, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, member-fpf-domain, fpf-trivial-subtype-top, fpf-domain wf, l member wf, subtype rel wf, fpf-ap wf, let wf, l-all-iff, event system wf, Id wf, fpf wf, Knd wf, top wf, es-kind wf, Kind-deq wf, fpf-cap wf, es-valtype wf, es-isrcv wf, assert wf, es-loc wf, es-E wf, id-deq wf, es-vartype wf, guard wf, es-decls wf